\documentclass{llncs}

\usepackage{url}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}


\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}

\newcommand{\text}[1]{\mbox{#1}}
\newcommand{\wc}{\_}
\newcommand{\mulstep}{ \stackrel{*}{\leadsto}}
\newcommand{\lam}[2]{\lambda #1 . #2}
\newcommand{\evals}[2]{#1 \downarrow #2}

\newcommand{\wm}[0]{\stackrel{\textit{w}}{\to}}
\newcommand{\interp}[1]{[\negthinspace[#1]\negthinspace]}
\newcommand{\symm}[1]{\langle\textit{#1}\rangle}
\newcommand{\rrl}[1]{\textit{r-#1}}
\newcommand{\rrlb}[0]{\textit{r-}\beta}
\newcommand{\trl}[1]{\textit{t-#1}}


\begin{document}
%\pagestyle{empty}
\title{Confluence of Lambda Calculus Modulo $\mu$-Equivalence}
\author{Peng Fu}
\institute{Computer Science, The University of Iowa}
\date{Oct 18, 2012}


\maketitle
\thispagestyle{empty}



\section{Syntax}

\begin{definition}[Terms]

\

\noindent $t \ :: = \ x \ |  \ \lambda x.t \ | \ t t'  \ | \ \mu t $


\end{definition}


\begin{definition}[Substitution]

\

\noindent $[t'/x] x \ : = \  t'$

\

\noindent $[t'/x]y \ := \ y $

\

\noindent $[t'/x]\lambda y.t\ : = \ \lambda y.[t'/x]t$

\

\noindent $[t'/x](t_1 t_2)\ : = \ [t'/x]t_1 [t'/x]t_2$

\

\noindent $[t'/x]\mu t \ := \mu ([t'/x]t)$

\end{definition}

\noindent \textbf{Remarks}: Capture avoiding and variable covention has to be assumed. The last definition, together with lemma \ref{pushin}, we have $[t'/x] \mu t =_{\mu} [\mu t'/x]\mu t $, which is totally fine since it is a congruence under mu-reduction, not something like $[t'/x] \mu t = [\mu t'/x]\mu t$. 

\begin{definition}[Beta-Reductions]

\

\noindent \infer{t \leadsto_{\beta} t}{}

\

\noindent \infer{(\lambda x.t)t' \leadsto_{\beta} [t''/x]t'''}{t \leadsto_{\beta} t'' & t' \leadsto_{\beta} t'''}

\

\noindent \infer{\lambda x.t \leadsto_{\beta} \lambda x.t'}{t \leadsto_{\beta}t' }

\

\noindent \infer{t t' \leadsto_{\beta} t'' t'''}{t \leadsto_{\beta}t'' & t' \leadsto_{\beta} t'''}

\

\noindent \infer{\mu t \leadsto_{\beta} \mu t'}{t \leadsto_{\beta}t' }

\end{definition}

\noindent \textbf{Remarks}: Here the notion of beta reduction is a direct extension 
of Tait-Martin L\"of's notion of parallel reduction just by adding the last congruence rule about the $\mu$. So it should be clear that beta reductions alone is confluent. 

\begin{definition}[Mu-Reductions]

\

\noindent \infer{ \mu(\lambda x.t) \leadsto_{\mu} \lambda x.\mu t}{}

\

\noindent \infer{ \mu((t_1 t_2) t_3 ) \leadsto_{\mu} (\mu (t_1 t_2)) (\mu t_3)}{}

\

\noindent \infer{ \mu((\lambda x.t_1) t_2 ) \leadsto_{\mu}  (\lambda x.\mu t_1) (\mu t_2)}{}

\

\noindent \infer{ \mu( \mu t ) \leadsto_{\mu} \mu t}{}

\

\noindent \infer{\lambda x.t \leadsto_{\mu} \lambda x.t'}{t \leadsto_{\mu} t'}

\

\noindent \infer{t t' \leadsto_{\mu} t'' t'''}{t \leadsto_{\mu} t'' & t' \leadsto_{\mu} t''}

\

\noindent \infer{\mu t \leadsto_{\mu} \mu t'}{t \leadsto_{\mu}t' }

\

\noindent \infer{ t \leadsto_{\mu}  t}{}

\end{definition}

\begin{definition}
We write $t =_{\mu} t'$ if there exist a $t''$ such that $t \stackrel{*}{\leadsto}_{\mu} t''$ and $t' \stackrel{*}{\leadsto}_{\mu} t''$.

\end{definition}

\section{Confluence}
\begin{lemma}
$\leadsto_{\mu}$ satisfies the diamond property.
\end{lemma}
\begin{proof}
By induction on the derivation of $\leadsto_{\mu}$.
\end{proof}


\begin{lemma}
If $t \leadsto_{\mu} t'$, then $[t''/x]t \leadsto_{\mu} [t''/x]t'$.

\end{lemma}

\begin{proof}
By induction on the derivation of $t \leadsto_{\mu} t'$.
\end{proof}

\begin{lemma}
\label{subst}
If $t =_{\mu} t'$, then $[t''/x]t =_{\mu} [t''/x]t'$.

\end{lemma}

\begin{lemma}
\label{pushin}
$\mu ([t_2/x]t_1) = _{\mu} [\mu t_2 /x]\mu t_1$.

\end{lemma}

\begin{proof}
\noindent By induction on the structure of $t_1$.

\

\noindent \underline{Base Case}: $t = x$. 

\

\noindent LHS is $\mu t_2$, RHS is $\mu \mu t_2$. Thus $\mu t_2 =_{\mu} \mu \mu t_2$.

\

\noindent \underline{Step Case}: $t = t_3 t_4$. 

\

\noindent  $\mu ([t_2/x](t_3 t_4)) = \mu ([t_2/x]t_3 [t_2/x]t_4) =_{\mu} (\mu [t_2/x]t_3)(\mu [t_2/x]t_4) =_{IH} ([\mu t_2/x]\mu t_3)([\mu t_2/x]\mu t_4) =_{\mu} [\mu t_2/x](\mu t_3 \mu t_4)) =_{\mu} [\mu t_2/x](\mu (t_3 t_4))$. 

\

\noindent The last equality is because of lemma \ref{subst}. 

\

\noindent \underline{Step Case}: $t = \lambda y.t$

\

\noindent $\mu ([t'/x] (\lambda y.t)) = \mu (\lambda y.[t'/x]t) =_{\mu} \lambda y.(\mu [t'/x]t) =_{IH} \lambda y. ([\mu t'/x]\mu t) = [\mu t'/x] (\lambda y.\mu t) =_{\mu} [\mu t'/x]\mu (\lambda y.t) $. 

\

\noindent \underline{Step Case}: $t = \mu t$

\

\noindent $\mu ([t'/x]\mu t) = \mu (\mu [t'/x]t) =_{IH} \mu ([\mu t'/x]\mu t) =[\mu t'/x] (\mu \mu t)  $


\end{proof}

\begin{lemma}
If $t_1 \leadsto_{\mu}  t_1' $, then $[t_1/x]t \leadsto_{\mu} [t_1' /x] t$.

\end{lemma}

\begin{proof}
Directly by induction on the structure of $t$. 
\end{proof}

\begin{lemma}
If $t_1 =_{\mu}  t_1' $, then $[t_1/x]t =_{\mu} [t_1' /x] t$.

\end{lemma}

\begin{proof}
By the lemma above.


\end{proof}


\begin{lemma}
If $t_1 = _{\mu}  t_1' $ and $t_2 = _{\mu}  t_2' $, then $[t_2/x]t_1 = _{\mu} [t_2' /x] t_1'$.

\end{lemma}

\begin{proof}
\noindent $[t_2/x]t_1 = _{\mu} [t_2/x] t_1'=_{\mu} [t_2' /x] t_1'$.
\end{proof}

\begin{lemma}
\label{tile}
If $t_1 \leadsto_{\mu} t_1'$ and $t_1 \leadsto_{\beta} t_2$, then there exists a $t_2'$ such that $t_1' \leadsto_{\beta} t_2'$ and $t_2 =_{\mu} t_2'$.

\end{lemma}

\begin{proof}
By induction on the derivation of $t_1 \leadsto_{\beta} t_2$ and inversion on $t_1 \leadsto_{\mu} t_1'$. 


\end{proof}

\begin{lemma}
\label{cotile}
If $t_1' \leadsto_{\mu} t_1$ and $t_1 \leadsto_{\beta} t_2$, then there exists a $t_2'$ such that $t_1' \leadsto_{\beta} t_2'$ and $t_2 =_{\mu} t_2'$.

\end{lemma}

\begin{proof}
By induction on the derivation of $t_1 \leadsto_{\beta} t_2$ and inversion on $t_1' \leadsto_{\mu} t_1$. 

\end{proof}




\begin{theorem}[Modularity]
If $t_1 =_{\mu} t_1'$ and $t_1 \leadsto_{\beta} t_2$, then there exists a $t_2'$ such that $t_1' \leadsto_{\beta} t_2'$ and $t_2 =_{\mu} t_2'$.

\end{theorem}

\begin{proof}
By lemma \ref{tile} and lemma \ref{cotile}. 

\end{proof}

\noindent Since $t \leadsto_{\mu} t'$ implies $t =_{\mu} t'$, use the modularity theorem, we can do some tiling to prove the confluence of the whole system. 

\end{document}
